The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^2).

(0) Obligation:

The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^2).


The TRS R consists of the following rules:

nonZero(0) → false
nonZero(s(x)) → true
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
id_inc(x) → x
id_inc(x) → s(x)
random(x) → rand(x, 0)
rand(x, y) → if(nonZero(x), x, y)
if(false, x, y) → y
if(true, x, y) → rand(p(x), id_inc(y))

Rewrite Strategy: INNERMOST

(1) TrsToWeightedTrsProof (BOTH BOUNDS(ID, ID) transformation)

Transformed TRS to weighted TRS

(2) Obligation:

The Runtime Complexity (innermost) of the given CpxWeightedTrs could be proven to be BOUNDS(1, n^2).


The TRS R consists of the following rules:

nonZero(0) → false [1]
nonZero(s(x)) → true [1]
p(s(0)) → 0 [1]
p(s(s(x))) → s(p(s(x))) [1]
id_inc(x) → x [1]
id_inc(x) → s(x) [1]
random(x) → rand(x, 0) [1]
rand(x, y) → if(nonZero(x), x, y) [1]
if(false, x, y) → y [1]
if(true, x, y) → rand(p(x), id_inc(y)) [1]

Rewrite Strategy: INNERMOST

(3) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)

Infered types.

(4) Obligation:

Runtime Complexity Weighted TRS with Types.
The TRS R consists of the following rules:

nonZero(0) → false [1]
nonZero(s(x)) → true [1]
p(s(0)) → 0 [1]
p(s(s(x))) → s(p(s(x))) [1]
id_inc(x) → x [1]
id_inc(x) → s(x) [1]
random(x) → rand(x, 0) [1]
rand(x, y) → if(nonZero(x), x, y) [1]
if(false, x, y) → y [1]
if(true, x, y) → rand(p(x), id_inc(y)) [1]

The TRS has the following type information:

nonZero :: 0:s → false:true 0 :: 0:s false :: false:true s :: 0:s → 0:s true :: false:true p :: 0:s → 0:s id_inc :: 0:s → 0:s random :: 0:s → 0:s rand :: 0:s → 0:s → 0:s if :: false:true → 0:s → 0:s → 0:s

Rewrite Strategy: INNERMOST

(5) CompletionProof (UPPER BOUND(ID) transformation)

The TRS is a completely defined constructor system, as every type has a constant constructor and the following rules were added:

p(v0) → null_p [0]
nonZero(v0) → null_nonZero [0]
if(v0, v1, v2) → null_if [0]

And the following fresh constants:

null_p, null_nonZero, null_if

(6) Obligation:

Runtime Complexity Weighted TRS where all functions are completely defined. The underlying TRS is:

Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: nonZero(0) → false [1] nonZero(s(x)) → true [1] p(s(0)) → 0 [1] p(s(s(x))) → s(p(s(x))) [1] id_inc(x) → x [1] id_inc(x) → s(x) [1] random(x) → rand(x, 0) [1] rand(x, y) → if(nonZero(x), x, y) [1] if(false, x, y) → y [1] if(true, x, y) → rand(p(x), id_inc(y)) [1] p(v0) → null_p [0] nonZero(v0) → null_nonZero [0] if(v0, v1, v2) → null_if [0] The TRS has the following type information: nonZero :: 0:s:null_p:null_if → false:true:null_nonZero 0 :: 0:s:null_p:null_if false :: false:true:null_nonZero s :: 0:s:null_p:null_if → 0:s:null_p:null_if true :: false:true:null_nonZero p :: 0:s:null_p:null_if → 0:s:null_p:null_if id_inc :: 0:s:null_p:null_if → 0:s:null_p:null_if random :: 0:s:null_p:null_if → 0:s:null_p:null_if rand :: 0:s:null_p:null_if → 0:s:null_p:null_if → 0:s:null_p:null_if if :: false:true:null_nonZero → 0:s:null_p:null_if → 0:s:null_p:null_if → 0:s:null_p:null_if null_p :: 0:s:null_p:null_if null_nonZero :: false:true:null_nonZero null_if :: 0:s:null_p:null_if Rewrite Strategy: INNERMOST

(7) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID) transformation)

Transformed the TRS into an over-approximating RNTS by (improved) Size Abstraction.
The constant constructors are abstracted as follows:

0 => 0
false => 1
true => 2
null_p => 0
null_nonZero => 0
null_if => 0

(8) Obligation:

Complexity RNTS consisting of the following rules:

id_inc(z) -{ 1 }→ x :|: x >= 0, z = x
id_inc(z) -{ 1 }→ 1 + x :|: x >= 0, z = x
if(z, z', z'') -{ 1 }→ y :|: z' = x, z'' = y, z = 1, x >= 0, y >= 0
if(z, z', z'') -{ 1 }→ rand(p(x), id_inc(y)) :|: z = 2, z' = x, z'' = y, x >= 0, y >= 0
if(z, z', z'') -{ 0 }→ 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0
nonZero(z) -{ 1 }→ 2 :|: x >= 0, z = 1 + x
nonZero(z) -{ 1 }→ 1 :|: z = 0
nonZero(z) -{ 0 }→ 0 :|: v0 >= 0, z = v0
p(z) -{ 1 }→ 0 :|: z = 1 + 0
p(z) -{ 0 }→ 0 :|: v0 >= 0, z = v0
p(z) -{ 1 }→ 1 + p(1 + x) :|: x >= 0, z = 1 + (1 + x)
rand(z, z') -{ 1 }→ if(nonZero(x), x, y) :|: x >= 0, y >= 0, z = x, z' = y
random(z) -{ 1 }→ rand(x, 0) :|: x >= 0, z = x

Only complete derivations are relevant for the runtime complexity.

(9) CompleteCoflocoProof (EQUIVALENT transformation)

Transformed the RNTS (where only complete derivations are relevant) into cost relations for CoFloCo:

eq(start(V, V6, V9),0,[nonZero(V, Out)],[V >= 0]). eq(start(V, V6, V9),0,[p(V, Out)],[V >= 0]). eq(start(V, V6, V9),0,[fun(V, Out)],[V >= 0]). eq(start(V, V6, V9),0,[random(V, Out)],[V >= 0]). eq(start(V, V6, V9),0,[rand(V, V6, Out)],[V >= 0,V6 >= 0]). eq(start(V, V6, V9),0,[if(V, V6, V9, Out)],[V >= 0,V6 >= 0,V9 >= 0]). eq(nonZero(V, Out),1,[],[Out = 1,V = 0]). eq(nonZero(V, Out),1,[],[Out = 2,V1 >= 0,V = 1 + V1]). eq(p(V, Out),1,[],[Out = 0,V = 1]). eq(p(V, Out),1,[p(1 + V2, Ret1)],[Out = 1 + Ret1,V2 >= 0,V = 2 + V2]). eq(fun(V, Out),1,[],[Out = V3,V3 >= 0,V = V3]). eq(fun(V, Out),1,[],[Out = 1 + V4,V4 >= 0,V = V4]). eq(random(V, Out),1,[rand(V5, 0, Ret)],[Out = Ret,V5 >= 0,V = V5]). eq(rand(V, V6, Out),1,[nonZero(V7, Ret0),if(Ret0, V7, V8, Ret2)],[Out = Ret2,V7 >= 0,V8 >= 0,V = V7,V6 = V8]). eq(if(V, V6, V9, Out),1,[],[Out = V10,V6 = V11,V9 = V10,V = 1,V11 >= 0,V10 >= 0]). eq(if(V, V6, V9, Out),1,[p(V12, Ret01),fun(V13, Ret11),rand(Ret01, Ret11, Ret3)],[Out = Ret3,V = 2,V6 = V12,V9 = V13,V12 >= 0,V13 >= 0]). eq(p(V, Out),0,[],[Out = 0,V14 >= 0,V = V14]). eq(nonZero(V, Out),0,[],[Out = 0,V15 >= 0,V = V15]). eq(if(V, V6, V9, Out),0,[],[Out = 0,V16 >= 0,V9 = V17,V18 >= 0,V = V16,V6 = V18,V17 >= 0]). input_output_vars(nonZero(V,Out),[V],[Out]). input_output_vars(p(V,Out),[V],[Out]). input_output_vars(fun(V,Out),[V],[Out]). input_output_vars(random(V,Out),[V],[Out]). input_output_vars(rand(V,V6,Out),[V,V6],[Out]). input_output_vars(if(V,V6,V9,Out),[V,V6,V9],[Out]).

CoFloCo proof output:
Preprocessing Cost Relations
=====================================

#### Computed strongly connected components
0. non_recursive : [fun/2]
1. recursive : [p/2]
2. non_recursive : [nonZero/2]
3. recursive : [if/4,rand/3]
4. non_recursive : [random/2]
5. non_recursive : [start/3]

#### Obtained direct recursion through partial evaluation
0. SCC is partially evaluated into fun/2
1. SCC is partially evaluated into p/2
2. SCC is partially evaluated into nonZero/2
3. SCC is partially evaluated into rand/3
4. SCC is completely evaluated into other SCCs
5. SCC is partially evaluated into start/3

Control-Flow Refinement of Cost Relations
=====================================

### Specialization of cost equations fun/2
* CE 13 is refined into CE [21]
* CE 14 is refined into CE [22]


### Cost equations --> "Loop" of fun/2
* CEs [21] --> Loop 13
* CEs [22] --> Loop 14

### Ranking functions of CR fun(V,Out)

#### Partial ranking functions of CR fun(V,Out)


### Specialization of cost equations p/2
* CE 10 is refined into CE [23]
* CE 12 is refined into CE [24]
* CE 11 is refined into CE [25]


### Cost equations --> "Loop" of p/2
* CEs [25] --> Loop 15
* CEs [23,24] --> Loop 16

### Ranking functions of CR p(V,Out)
* RF of phase [15]: [V-1]

#### Partial ranking functions of CR p(V,Out)
* Partial RF of phase [15]:
- RF of loop [15:1]:
V-1


### Specialization of cost equations nonZero/2
* CE 19 is refined into CE [26]
* CE 20 is refined into CE [27]
* CE 18 is refined into CE [28]


### Cost equations --> "Loop" of nonZero/2
* CEs [26] --> Loop 17
* CEs [27] --> Loop 18
* CEs [28] --> Loop 19

### Ranking functions of CR nonZero(V,Out)

#### Partial ranking functions of CR nonZero(V,Out)


### Specialization of cost equations rand/3
* CE 17 is refined into CE [29]
* CE 15 is refined into CE [30,31,32]
* CE 16 is refined into CE [33,34,35,36]


### Cost equations --> "Loop" of rand/3
* CEs [36] --> Loop 20
* CEs [35] --> Loop 21
* CEs [34] --> Loop 22
* CEs [33] --> Loop 23
* CEs [29] --> Loop 24
* CEs [30,31,32] --> Loop 25

### Ranking functions of CR rand(V,V6,Out)
* RF of phase [20,21]: [V-1]

#### Partial ranking functions of CR rand(V,V6,Out)
* Partial RF of phase [20,21]:
- RF of loop [20:1,21:1]:
V-1


### Specialization of cost equations start/3
* CE 3 is refined into CE [37,38,39,40,41,42,43,44,45,46,47,48,49,50]
* CE 2 is refined into CE [51]
* CE 4 is refined into CE [52]
* CE 5 is refined into CE [53,54,55]
* CE 6 is refined into CE [56,57]
* CE 7 is refined into CE [58,59]
* CE 8 is refined into CE [60,61,62,63,64,65]
* CE 9 is refined into CE [66,67,68,69,70,71]


### Cost equations --> "Loop" of start/3
* CEs [37,38,39,40,41,42,43,44,45,46,47,48,49,50] --> Loop 26
* CEs [52] --> Loop 27
* CEs [51,53,54,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,70,71] --> Loop 28

### Ranking functions of CR start(V,V6,V9)

#### Partial ranking functions of CR start(V,V6,V9)


Computing Bounds
=====================================

#### Cost of chains of fun(V,Out):
* Chain [14]: 1
with precondition: [V+1=Out,V>=0]

* Chain [13]: 1
with precondition: [V=Out,V>=0]


#### Cost of chains of p(V,Out):
* Chain [[15],16]: 1*it(15)+1
Such that:it(15) =< Out

with precondition: [Out>=1,V>=Out+1]

* Chain [16]: 1
with precondition: [Out=0,V>=0]


#### Cost of chains of nonZero(V,Out):
* Chain [19]: 1
with precondition: [V=0,Out=1]

* Chain [18]: 0
with precondition: [Out=0,V>=0]

* Chain [17]: 1
with precondition: [Out=2,V>=1]


#### Cost of chains of rand(V,V6,Out):
* Chain [[20,21],25]: 10*it(20)+1*s(5)+1*s(6)+2
Such that:aux(5) =< V
it(20) =< aux(5)
aux(2) =< aux(5)
s(5) =< it(20)*aux(5)
s(6) =< it(20)*aux(2)

with precondition: [Out=0,V>=2,V6>=0]

* Chain [[20,21],23,25]: 10*it(20)+1*s(5)+1*s(6)+7
Such that:aux(6) =< V
it(20) =< aux(6)
aux(2) =< aux(6)
s(5) =< it(20)*aux(6)
s(6) =< it(20)*aux(2)

with precondition: [Out=0,V>=2,V6>=0]

* Chain [[20,21],23,24]: 10*it(20)+1*s(5)+1*s(6)+8
Such that:aux(7) =< V
it(20) =< aux(7)
aux(2) =< aux(7)
s(5) =< it(20)*aux(7)
s(6) =< it(20)*aux(2)

with precondition: [V>=2,V6>=0,Out>=V6+1,V+V6>=Out]

* Chain [[20,21],22,25]: 10*it(20)+1*s(5)+1*s(6)+7
Such that:aux(8) =< V
it(20) =< aux(8)
aux(2) =< aux(8)
s(5) =< it(20)*aux(8)
s(6) =< it(20)*aux(2)

with precondition: [Out=0,V>=2,V6>=0]

* Chain [[20,21],22,24]: 10*it(20)+1*s(5)+1*s(6)+8
Such that:aux(9) =< V
it(20) =< aux(9)
aux(2) =< aux(9)
s(5) =< it(20)*aux(9)
s(6) =< it(20)*aux(2)

with precondition: [V>=2,V6>=0,Out>=V6,V+V6>=Out+1]

* Chain [25]: 2
with precondition: [Out=0,V>=0,V6>=0]

* Chain [24]: 3
with precondition: [V=0,V6=Out,V6>=0]

* Chain [23,25]: 7
with precondition: [Out=0,V>=1,V6>=0]

* Chain [23,24]: 8
with precondition: [Out=V6+1,V>=1,Out>=1]

* Chain [22,25]: 7
with precondition: [Out=0,V>=1,V6>=0]

* Chain [22,24]: 8
with precondition: [V6=Out,V>=1,V6>=0]


#### Cost of chains of start(V,V6,V9):
* Chain [28]: 101*s(22)+10*s(26)+10*s(27)+9
Such that:aux(11) =< V
s(22) =< aux(11)
s(25) =< aux(11)
s(26) =< s(22)*aux(11)
s(27) =< s(22)*s(25)

with precondition: [V>=0]

* Chain [27]: 1
with precondition: [V=1,V6>=0,V9>=0]

* Chain [26]: 110*s(63)+10*s(67)+10*s(68)+11
Such that:aux(18) =< V6
s(63) =< aux(18)
s(66) =< aux(18)
s(67) =< s(63)*aux(18)
s(68) =< s(63)*s(66)

with precondition: [V=2,V6>=0,V9>=0]


Closed-form bounds of start(V,V6,V9):
-------------------------------------
* Chain [28] with precondition: [V>=0]
- Upper bound: 101*V+9+20*V*V
- Complexity: n^2
* Chain [27] with precondition: [V=1,V6>=0,V9>=0]
- Upper bound: 1
- Complexity: constant
* Chain [26] with precondition: [V=2,V6>=0,V9>=0]
- Upper bound: 110*V6+11+20*V6*V6
- Complexity: n^2

### Maximum cost of start(V,V6,V9): max([101*V+8+20*V*V,nat(V6)*110+10+nat(V6)*20*nat(V6)])+1
Asymptotic class: n^2
* Total analysis performed in 347 ms.

(10) BOUNDS(1, n^2)